Skip to content

Add flag --emit-json-spec to kprovex#2428

Merged
rv-jenkins merged 15 commits intomasterfrom
emit-json-kprovex
Feb 12, 2022
Merged

Add flag --emit-json-spec to kprovex#2428
rv-jenkins merged 15 commits intomasterfrom
emit-json-kprovex

Conversation

@ehildenb
Copy link
Copy Markdown
Member

@ehildenb ehildenb commented Feb 8, 2022

Fixes: #2288

This PR does:

  • Add flag to kprovex called --emit-json-spec which emits the spec module as JSON to the specified file.
  • Fixes the JSON serialization of KImport to include the node header (all KAST JSON terms must have node header).
  • Adds unit tests of the pyk library which do:
    • Serialize pretty proof to json using new flag -> read json proof in pyk and write out as pretty to file -> run kprovex on the newly serialized proof using pyks KProve.prove()
    • Serialize pretty proof to json using new flag -> read json proof in pyk and prove using KProve.proveClaim().

Comment thread kernel/src/main/java/org/kframework/kprovex/KProve.java Outdated
@ehildenb ehildenb marked this pull request as ready for review February 11, 2022 00:24
@ehildenb
Copy link
Copy Markdown
Member Author

@radumereuta this is ready for review.

@ehildenb ehildenb assigned ehildenb and unassigned tothtamas28 Feb 11, 2022
@rv-jenkins rv-jenkins merged commit f49fed0 into master Feb 12, 2022
@rv-jenkins rv-jenkins deleted the emit-json-kprovex branch February 12, 2022 01:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Support dumping json empty configuration at kompile time

4 participants